fpf-ap(fpf-join(id-deq;
fpf-ap(fpf-join(fpf-single(mkid{x1:ut2}; int_seg(0; 3));
fpf-ap(fpf-join(fpf-join(id-deq;
fpf-ap(fpf-join(fpf-join(fpf-single(mkid{v1:ut2}; int_seg(0; 3));
fpf-ap(fpf-join(fpf-join(fpf-join(id-deq;
fpf-ap(fpf-join(fpf-join(fpf-join(fpf-single(mkid{win:ut2}; );
fpf-ap(fpf-join(fpf-join(fpf-join(fpf-join(id-deq;
fpf-ap(fpf-join(fpf-join(fpf-join(fpf-join(fpf-single(mkid{x2:ut2}; int_seg(0; 3));
fpf-ap(fpf-join(fpf-join(fpf-join(fpf-join(fpf-single(mkid{v2:ut2}; int_seg(0; 3))))));
fpf-ap(id-deq;
fpf-ap(mkid{v1:ut2}) 

latex

Definitions	fpf-join(eq; f; g), fpf-ap(f; eq; x), fpf-cap(f; eq; x; z), int_seg(i; j), , {x:A| B(x)} , A, False, P  Q, x:AB(x), void, lelt(i; j; k), P  Q, x:A  B(x), A  B, x:A. B(x), a < b, t  T, #$n
Lemmas	le wf